\documentclass[xcolor=dvipsnames,mathserif,svgnames,11pt]{beamer}

% for a handout:
%
%\documentclass[handout,11pt]{beamer}
%
%\usepackage{pgfpages}
%\pgfpagesuselayout{2 on 1}[letterpaper,border shrink=5mm]

\usepackage{diagrams}
\usepackage{listings}
\usepackage{proof}
\lstdefinelanguage{MyHaskell}
{alsoletter={+,|,->, =, ::}, morekeywords={+,|,->, =, ::, data, Int, max, case, of, forall, theorem, proof}
}


\lstdefinelanguage{MyLambda}
{alsoletter={\., |, ->, = }, morekeywords={=,|, -> ,\., lam , fix, case, of}}


%\lstset{language=MyHaskell, keywordstyle=\color{scyan},basicstyle=\ttfamily}

\definecolor{syellow}{RGB}{181,137,0}
\definecolor{scyan}{RGB}{42,161,152}

\DefineNamedColor{named}{MyBlue}{RGB}{38,139,210}
\DefineNamedColor{named}{Base3}{RGB}{253,246,227}
\DefineNamedColor{named}{Base00}{RGB}{101,123,131}
\newcommand{\cemph}[1]{\textcolor{Blue}{#1}}
\newcommand{\remph}[1]{\textcolor{Blue}{#1}}
\newcommand{\ep}[0]{\epsilon}
\newcommand{\selfstar}[0]{\mathsf{Selfstar}}
\newcommand{\uemph}[1]{\underline{#1}}
\newcommand{\mlstep}[1]{\twoheadrightarrow_{\underline{#1}}}
\newcommand{\lstep}[1]{\to_{\underline{#1}}}
\newcommand{\mstep}[1]{\twoheadrightarrow_{#1}}
\newcommand{\m}[2]{ \{\mu_{#1}\}_{#1 \in #2}} 
\newcommand{\M}[3]{\{#1_i \mapsto #2_i\}_{i \in #3}} 
\newcommand{\bm}[4]{
\{(#1_i:#2_i) \mapsto #3_i\}_{i \in #4}} 
\newarrowfiller{dasheq} {==}{==}{==}{==}
\newarrow {Mapsto} |--->
\newarrow {Line} -----
\newarrow {Implies} ===={=>}
\newarrow {EImplies} {}{dasheq}{}{dasheq}{=>}
\newarrow {Onto} ----{>>}
\newarrow {Dashto}{}{dash}{}{dash}{>}
\newarrow {Dashtoo}{}{dash}{}{dash}{>>}


\mode<presentation>
{
  %\usetheme{Warsaw}
  % or ...
%gets rid of bottom navigation bars
%\setbeamertemplate{footline}[page number]{}

%gets rid of navigation symbols
\setbeamertemplate{navigation symbols}{}
\setbeamertemplate{footline}[frame number]
\usetheme{default}
%\usecolortheme[named=MyBlue]{structure}
%\setbeamercolor{background canvas}{bg=Base3}
%\setbeamercolor{normal text}{fg=Base00}

%\usetheme{Edinburgh}

%  \setbeamercovered{transparent}
  % or whatever (possibly just delete it)
}

\usepackage[english]{babel}
\usepackage[latin1]{inputenc}
\usepackage{times}
\usepackage[T1]{fontenc}
% Or whatever. Note that the encoding and the font should match. If T1
% does not look nice, try deleting the line with the fontenc.

\title[Prop]
{Lambda Encoding in Type Theory \`a la Curry}

\author{Peng Fu}

\institute[University of Iowa]
{ Advisor: Prof. Aaron Stump \\ 
  Dept. of Computer Science\\ }
\date{}
%\date{May 22, 2013 }
% If you have a file called "university-logo-filename.xxx", where xxx
% is a graphic format that can be processed by latex or pdflatex,
% resp., then you can add a logo as follows:

% \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
% \logo{\pgfuseimage{university-logo}}



% Delete this, if you do not want the table of contents to pop up at
% the beginning of each subsection:
%\AtBeginSubsection[]
%{
%  \begin{frame}<beamer>
%    \frametitle{Outline}
%    \tableofcontents[currentsection,currentsubsection]
%  \end{frame}
%}


% If you wish to uncover everything in a step-wise fashion, uncomment
% the following command: 

%\beamerdefaultoverlayspecification{<+->}

\begin{document}

\begin{frame}[plain]
  \titlepage
\end{frame}

%% \begin{frame}
%% \frametitle{Prelude: Programs and Data}

%%     \begin{figure}
%%      \includegraphics{von-neumann.jpeg}
%%      \end{figure}
%% \end{frame}

%% \begin{frame}[fragile]
%% \frametitle{Prelude: Programs and Data}
%%     Buffer overflow(Data as Program)
%%     \begin{lstlisting}[language=C,keywordstyle=\color{SeaGreen},basicstyle=\ttfamily]
%%       #include <string.h>
%%       void foo (char *bar)
%%       {
%%         char  c[12];
%%         strcpy(c, bar);  // no bounds checking...
%%       }
%%       int main (int argc, char **argv)
%%       {
%%         foo(argv[1]); 
%%       }
%%     \end{lstlisting}
%% \end{frame}
\begin{frame}
  \frametitle{Introduction}
  Features of functional programming languages.
  \begin{itemize}
  \item Algebraic data type.
  \item Program by pattern matching, recursion and functional application.
  \item Type inference.
  \end{itemize}

\end{frame}

\begin{frame}[fragile]
  \frametitle{Introduction}
\begin{itemize}  
\item<1-> Example.
\begin{lstlisting}[language=MyHaskell, keywordstyle=\color{Blue},basicstyle=\ttfamily]
data Nat = Zero
          | Succ Nat
add :: Nat-> Nat -> Nat
add Zero m = m
add (Succ n) m = Succ (add n m)
\end{lstlisting}
  \item<2-> Prove properties about programs.
    \begin{lstlisting}[language=MyHaskell, keywordstyle=\color{Blue},basicstyle=\ttfamily]
theorem : forall n :: Nat. add n Zero = n
proof : induction on n...
    \end{lstlisting}
\end{itemize}

%% $\tt{add}$ is usually translated to:

%% \

%% \begin{lstlisting}[language=MyHaskell, keywordstyle=\color{Blue},basicstyle=\ttfamily]
%% add n m = case n of
%%           Zero -> m
%%          | Succ p -> Succ (add p m)
%% \end{lstlisting}
\end{frame}

% n = Zero => 
%%    add Zero Zero = Zero by evaluation.
%%  n = Succ n' =>
%%    add (Succ n') Zero = Succ (add n' Zero) 
%%      by evaluation.
%%    add n' Zero = n'
%%      by induction hypothesis.
%%    Succ (add n' Zero) = Succ n' 
%%      by congruence.
%%    Thus, add (Succ n') Zero = Succ n' 
%% Q.E.D. 

\begin{frame}
\frametitle{Introduction}
\begin{itemize}
\item<1-> How to implement such reasoning feature?
\begin{itemize}
\item Primitive user defined data type.
\item Build-in induction principle. 
\end{itemize}
\item<2-> Why this is not good? 
\begin{itemize}
\item Really complicated design.
\item Hard to prove properties about the language.
\end{itemize}
\item<3-> Motivations for my dissertation. 
\begin{itemize}
\item Adopt a simple system.
\item Derive algebraic data from the system.
\item Derive induction principle from the system.
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Outline}

\begin{itemize}
\item \remph{Fundamental Concepts}
%\item Typed Lambda encoding
\item A Framework for Internalizing Relations into Type Theory
\item Dependently Typed Programming with Scott Encoding
\item Church Encoding with Dependent Type
\item Lambda Encoding with Comprehension
\item Future Works
\end{itemize}

\end{frame}
\begin{frame}
\frametitle{Fundamental Concepts}

\begin{itemize}
\item Lambda Encodings: Church encoding and Scott encoding.
  \begin{itemize}
    \item Lambda term $t \ ::= \ x \ | \ \lambda x.t \ | \ t\ t'$
  \item Church numeral $\bar{3}$: $\lambda s.\lambda z. s\ (s \ (s\ z))$
  \item Scott numeral $\bar{3}$: $\lambda s.\lambda z. s\ \bar{2}$
  \item Scott-Church numeral $\bar{3}$: $\lambda s.\lambda z. s\ \bar{2} (s\ \bar{1} (s\ \bar{0}\ z))$
  \end{itemize}
\item Term rewrite system and Church-Rosser property. 
  \begin{center}
\begin{tabular}{lll}
\begin{diagram}[size=1.5em,textflow]
 & & a & & \\
 & \ldOnto & & \rdOnto &  \\
 b & &  &  & c \\
 & \rdDashtoo & & \ldDashtoo &  \\
 & & d & & \\
\end{diagram}
\end{tabular}  
\end{center}
\item Type systems \`a la Curry. 
  \begin{itemize}
  \item Unannotated v.s. Annotated
  \item $\lambda x.x$ v.s. $\lambda x:T.x$
  \end{itemize}
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Outline}

\begin{itemize}
\item Fundamental Concepts
%\item Typed Lambda encoding
\item \remph{A Framework for Internalizing Relations into Type Theory}
\item Dependently Typed Programming with Scott Encoding
\item Church Encoding with Dependent Type
\item Lambda Encoding with Comprehension
\item Future Works
\end{itemize}

\end{frame}

%% \begin{frame}
%% \frametitle{Introduction: Lambda Calculus}

%% How about calling a function with an argument
%% \begin{itemize}
%% \item<1-> $f(a) = a + 1$ math
%% \item<2-> $(\lambda x.x+1)\ a \to_{\beta} a+1$ with lambda calculus
%% \item<3-> Explicit functional abstraction and application at syntactic level
%% \end{itemize}
%% \end{frame}


%% \begin{frame}
%% \frametitle{Introduction: Lambda Calculus}

%% Different angle to study lambda calculus


%% \begin{itemize}
%% \item<1-> Lambda calculus as foundation for mathematics. 
      
%% \item<2-> Semantics of lambda calculus

%% \item<3-> As a programming language with variant of $\beta$-reduction as 
%% operational semantics.

%% \item<4-> we will focus on the last angle.


%% \end{itemize}
%% \end{frame}

\begin{frame}
\frametitle{A Framework for Internalizing Relations into Type Theory}

\begin{itemize}
\item Enriched Types, internalization. 
  
  $T \ ::= X \ | \ T \to T' \ | \ \Pi x:T.T' \ | \ \forall X.T$
  
  $F \ ::= \ X \ | \ F \to F' \ | \ \Pi x:F.F' \ | \ \forall X.F\ | \cemph{\ t = t' \ | \ t \ep T \ | \ T <: T'}$
\item Prove consistency by normalization. 
\item Limitation: Unable to prove preservation without adding new rules.
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Outline}

\begin{itemize}
\item Fundamental Concepts
%\item Typed Lambda encoding
\item A Framework for Internalizing Relations into Type Theory
\item \remph{Dependently Typed Programming with Scott Encoding}
\item Church Encoding with Dependent Type
\item Lambda Encoding with Comprehension
\item Future Works
\end{itemize}

\end{frame}

\begin{frame}
\frametitle{Dependently Typed Programming with Scott Encoding}
\begin{itemize}
\item $\selfstar$.
  \begin{itemize}
  \item Self type.
    $T \ ::= X \ | \ T \to T' \ | \ \Pi x:T.T' \ | \ \forall X.T \ | \ \cemph{\iota x.T}$
  \item Self type mechanism
    \begin{tabular}{l}
      \infer={\Gamma\vdash t: [t/x]T}{\Gamma \vdash t : \iota x.T}
    \end{tabular}
  \end{itemize}
\item Results for $\selfstar$:
  \begin{itemize}
  \item Admit Scott-encoded data and Scott-Church data. 
  \item Type preservation and progress.
  \item Expressive dependent type programming language.
  \end{itemize}

\item Limitation: Inconsistent as a logic.
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Outline}

\begin{itemize}
\item Fundamental Concepts
%\item Typed Lambda encoding
\item A Framework for Internalizing Relations into Type Theory
\item Dependently Typed Programming with Scott Encoding
\item \remph{Church Encoding with Dependent Type}
\item Lambda Encoding with Comprehension
\item Future Works
\end{itemize}
\end{frame}


\begin{frame}
\frametitle{Church Encoding with Dependent Type}
System $\mathbf{S}$.
\begin{itemize}
  \item From Scott-Church numeral to Church numeral
    
    $\bar{3} \ := \lambda s.\lambda z. s\ \not\bar{2} (s\ \not\bar{1} (s\ \not\bar{0}\ z))$

\item Overcome the inconsistency by using implicit product.
      $T \ ::= X \ | \ T \to T' \ | \ \Pi x:T.T' \ | \ \forall X.T \ | \ \cemph{\iota x.T} \ | \ \cemph{\forall x:T'.T}$
  \begin{itemize}
  \item $\Pi x:T.T'$ v.s. $\forall x:T.T'$

    \
    
    \begin{tabular}{ll}
      \infer{\Gamma \vdash t\ t':[t'/x] T'}{\Gamma
\vdash t:\Pi x:T. T' & \Gamma \vdash t': T}

          &
      \infer{\Gamma \vdash t\not t':[t'/x] T'}{\Gamma
\vdash t:\forall x:T. T' & \Gamma \vdash t': T}
      
    \end{tabular}
  \end{itemize}
    \item Consistency system that admit Church-encoded data.
   \item Type preservation. 
    \item Limitation: Inefficient to retrieve subdata.
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Outline}

\begin{itemize}
\item Fundamental Concepts
%\item Typed Lambda encoding
\item A Framework for Internalizing Relations into Type Theory
\item Dependently Typed Programming with Scott Encoding
\item Church Encoding with Dependent Type
\item \remph{Lambda Encoding with Comprehension}
\item Future Works
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Lambda Encoding with Comprehension}
System $\mathfrak{G}$.
\begin{itemize}
\item A change of point of view:
  
  \begin{tabular}{l}
      \infer={\Gamma\vdash t: [t/x]T}{\Gamma \vdash t : \iota x.T}
    \end{tabular}
\item Comprehension: $t\ep \iota x.F \Leftrightarrow [t/x]F$
  \begin{itemize}
\item Formula $F\ ::= \ X \ | \ t \ep S \ | \ F \to F' \ | \ \forall x.F \ | \ \Pi X.F \ | \ \Pi Y.F$
    \item Set $S \ ::= \ Y \ | \ \iota x.F$
  \end{itemize}
  \item $t : \iota x.T$ becomes $t\ep \iota x.F$.
   \item Features:
     \begin{itemize}
     \item Consistent logical system.
     \item Be able to reason about Scott encoded data.
     \item No termination requirement for term.
     \end{itemize}
     \item Difference: Lambda term is untyped.
\end{itemize}

\end{frame}

\begin{frame}
\frametitle{Outline}

\begin{itemize}
\item Fundamental Concepts
%\item Typed Lambda encoding
\item A Framework for Internalizing Relations into Type Theory
\item Dependently Typed Programming with Scott Encoding
\item Church Encoding with Dependent Type
\item Lambda Encoding with Comprehension
\item \remph{Future Works}
\end{itemize}
\end{frame}


\begin{frame}
\frametitle{Future Works}

\begin{itemize}
\item Implementation of System $\mathfrak{G}$.
\item To include sets of set, relations, etc.
\item Consider the possibility of formula level computation.

\end{itemize}


\end{frame}


\begin{frame}
\frametitle{Last But Not Least}
Thank you very much for your time and being my dissertation committee!
\end{frame}


\end{document}



